import java.util.ArrayList;

import struct.Function;
import struct.Identity;
import struct.Rule;
import struct.Term;
import struct.Unifier;
import util.Utils;

public class Main {
    static Utils utils;
    
    public static void printUnified()
    {
    	System.out.println("Rules after unification: ");
    	for (int i = 0; i < Utils.betterWork.getRules().size(); i++)
        {
            System.out.println(Utils.betterWork.getRules().get(i));
        }
    }
    
    public static void printCPs(ArrayList<Rule> rules, int i)
    {
        String left = rules.get(i).getLeft().toString();
        String right1 = rules.get(i).getRight().toString();
        String right2 = left;
        for (int b = 0; b < Utils.betterWork.getRules().size(); b++)
        {
            Utils.betterWork.getRules().get(b).getLeft().setIndex(0);
        
        left = left.replace(
                Utils.betterWork.getRules().get(b).getLeft().toString(),
                Utils.betterWork.getRules().get(b).getRight().toString());
        right1 = right1.replace(
                Utils.betterWork.getRules().get(b).getLeft().toString(),
                Utils.betterWork.getRules().get(b).getRight().toString());
        }
        for(int b = 0; b < rules.size(); b++)
        {
            right2 = left.replace(
                    rules.get(b).getLeft().toString(),
                    rules.get(b).getRight().toString());
        }
      
        if (!left.equals(right1) && !left.equals(right2) && !right1.equals(right2))
        {
            System.out.println("CP: ");
            System.out.println(left + " -> " + right1);
            System.out.println(left + " -> " + right2);    
        }
    }
    public static void printCPs2(ArrayList<Rule> rules, int i)
    {
        Identity left = rules.get(i).getLeft().getTerm();
        Identity right1 = rules.get(i).getRight().getTerm();
        Identity right2 = left;
        for (int b = 0; b < Utils.betterWork.getRules().size(); b++)
        {
            Utils.betterWork.getRules().get(b).getLeft().setIndex(0);
        
        left = Utils.substitute(Utils.betterWork.getRules().get(b).getLeft().getTerm(),
               Utils.betterWork.getRules().get(b).getRight().getTerm(), left);
        right1 = Utils.substitute(Utils.betterWork.getRules().get(b).getLeft().getTerm(),
                 Utils.betterWork.getRules().get(b).getRight().getTerm(), right1);
        }
        for(int b = 0; b < rules.size(); b++)
        {
            right2 = Utils.substitute(rules.get(b).getLeft().getTerm(),
                     rules.get(b).getRight().getTerm(), left);
        }
      
        if (!left.equals(right1) && !left.equals(right2) && !right1.equals(right2))
        {
            System.out.println("CP: ");
            System.out.println(left + " -> " + right1);
            System.out.println(left + " -> " + right2);    
        }
    }
    
    
    public static void main(String[] args) {
        ArrayList<Rule> rules = Repository.generateRules2();
        ArrayList<Rule> renamed; 
        Utils.betterWork = new Unifier();
        
        renamed = Utils.renameRules(rules);
        for (int i = 0; i < renamed.size(); i++)
        {
        	for (int j = 0; j< rules.size(); j++)
        	{
        		ArrayList<Function> funx = Utils.getFunx(renamed.get(i));
        		for (int k = 0;  k < funx.size(); k++)
        		{
        			Rule rule = new Rule((Term)rules.get(j).getLeft().clone(), 
        					new Term((Function)funx.get(k).clone()));
        			System.out.println("solving rule: " + rule);
        			Utils.betterWork.solve(rule);
        			if (Utils.betterWork.getRules().size() > 0)
        			{
        			    printCPs2(rules, i);
        			}
        			//System.out.println("TRS after unification: ");
        			//printUnified();
        		}
        		Utils.betterWork.clearRules();
        	}
        }
        //printUnified();
    }
}
